$\forall$$A$:Type, $r$:($A$$\rightarrow$$A$$\rightarrow\mathbb{P}$), $B$:Type, $f$:($B$$\rightarrow$$A$). \\[0ex]WellFnd\{i\}($A$;$x$,$y$.$r$($x$,$y$)) $\Rightarrow$ WellFnd\{i\}($B$;$x$,$y$.$r$($f$($x$),$f$($y$)))